package fos

import scala.collection.mutable.{ Map, HashMap };

case class TypeError(msg: String) extends Exception(msg)

object Type {

  import CT._
  import Utils._

  type Class = String
  type Context = List[Pair[Class, String]]

  val OK = "OK"

  def typeOf(tree: Tree, ctx: Context): Class = {
    def stupidWarinig(cls: String, e: Expr): Unit = println("Stupid warining: (%s) %s".format(cls, e))
    def ClassDef(c: Class): ClassDef = Utils getClassDef c 
    def ClassDefExpr(args: List[Expr]): List[ClassDef] = args map (arg => ClassDef( typeOf(arg, ctx) ) )
    def ClassDefFields(fields: List[FieldDef]): List[ClassDef] = fields map (field => ClassDef( field.tpe ) )
    def Names(list: List[FieldDef]): List[Class] = list.map( _.name )
    def ::>>(D: List[ClassDef], C: List[ClassDef]): Boolean = (C zip D) forall (x => x._2 :> x._1 ) // C_i <: D_i for all i
    
    tree match {
      // EXPRESSION TYPING
      // (T-Var)
      case Var(name: String) => ctx.find(name == _._2) match {
        case Some(v) => v._1
        case None => throw TypeError("Variable %s not in context: %s" format (name, ctx))
      }
      // (T-Field)
      case Select(obj: Expr, field: String) => {
        val C0 = ClassDef( typeOf(obj, ctx) )
        C0.fields.find(_.name == field) match {
          case Some(f) => f.tpe
          case None => throw TypeError("Field %s not found in object %s" format (field, obj))
        }
      }
      case Apply(obj: Expr, method: String, args: List[Expr]) => {
        val C0 = ClassDef( typeOf(obj, ctx) )
        C0.findMethod(method) match {
          case Some(meth) => {
            val C = meth.tpe
            val C_ = ClassDefExpr(args)
            val D_ = ClassDefFields(meth.args)
            if (C_.length != D_.length) throw TypeError("Method args exeption for method %s of class %s. Recieved %s but expected %s".format(C0.name,method,C_.map(_.name), D_.map(_.name)))
            else if ( ! ::>>( D_, C_ ) ) throw TypeError("Method args length missmatch %s of class %s. Recieved %s but expected %s".format(C0.name,method,C_.map(_.name), D_.map(_.name)))
            else C 														// (T-Invk)
          }
          case None => throw TypeError("Method %s not found in %s".format(method, C0.name))
        }
      }
      // (T-New)
      case New(cls: String, args: List[Expr]) => {
        val C = ClassDef(cls)
        val C_ = ClassDefExpr(args)
        val D_ = ClassDefFields(C.fieldLookup)
        if (C_.length != D_.length) throw TypeError("Constructor args length missmatch for class %s. Recieved %s but expected %s".format(C.name,C_.map(_.name), D_.map(_.name)))
        else if ( ! ::>>( D_, C_ ) ) throw TypeError("Constructor args exeption for class %s. Recieved %s but expected %s".format(C.name,C_.map(_.name), D_.map(_.name)))
        else cls
      }
      // (T-UCast), (T-DCast) and (T-SCast)
      case Cast(cls: String, e: Expr) => {
        val C = ClassDef( cls )
        val D = ClassDef( typeOf(e, ctx) )
        if (C :> D) cls
        else if ((D :> C) && C != D) cls 
        else if (!(D :> C) && !(C :> D)) { stupidWarinig(cls, e); cls } 
        else throw TypeError("Cast error (%s) %s" format (cls, e))
      }
      
      // CLASS TYPING
      // (T-Class)
      case ClassDef(name: String, superclass: String, fields: List[FieldDef], ctor: CtrDef, methods: List[MethodDef]) => {
        val C = ClassDef( name )
        val C_ = ClassDefFields(fields)
        val f_ = Names( ClassDef(superclass).fieldLookup ::: fields )

        val D = ClassDef( superclass )
        val D_ = ClassDefFields(D.fieldLookup)
        val g_ = Names( D.fieldLookup )
        
        val M_ = methods
        
        // METHOD TYPING
        def OK_IN_C(met: MethodDef): Unit = met match {
          // (T-Method), throws exception if not 'OK IN C'
          case MethodDef(tpe: String, name: String, args: List[FieldDef], body: Expr) => {
            val C0 = ClassDef( tpe )
            val C_ = ClassDefFields(args)
            val x_ = Names( args )
            val E0 = ClassDef( typeOf( body, (C.name, "this") :: (C_.map(_.name) zip x_) ::: ctx ) )
            val D_ = ClassDefFields(args)
            val D0 = ClassDef( tpe )
            
            if ( !(C0 :> E0) ) throw TypeError("Method definition return type exception: declared as %s but expected %s".format(C0.name,E0.name))
            else if ( (C_ zip D_).exists(x => x._1!=x._2) || C_.length!=D_.length ) throw TypeError("Method definition args exception: declared as %s but expected %s".format(C_.map(_.name),D_.map(_.name)))
            else if ( C0 != D0 ) throw TypeError("Method definition return type exception: declared as %s but expected %s".format(C0.name,D0.name))
            else if (M_.count(_.name==name)!=1) throw TypeError("Method %s defined twice in %s".format(name,C.name))
          }
        }
        
        val obj = ClassDef("Object")
        def checkClassTree(other: ClassDef): Unit = other match {
          case `C` => throw TypeError("Class extends itself in the class recursion tree")
          case `obj` => Unit
          case other if C :> other => throw TypeError("Class extends itself in the class recursion tree")
          case other => checkClassTree( ClassDef(other.superclass) )
        }
        
        M_.foreach( OK_IN_C(_) ) 	// check (T-Method) for all methods
        if (C.name!=ctor.name) throw TypeError("Constructor naming exception for %s: declared as %s but expected %s".format(C.name,ctor.name,C.name))
        else if ( (g_ zip ctor.supers.map(_.name)).exists(x => x._1!=x._2) || g_.length!=ctor.supers.length ) throw TypeError("Constructor supers type exception: declared as %s but expected %s".format(ctor.supers.map(_.name),g_))
        else if ( f_ != Names( ctor.args ) ) throw TypeError("Constructor fields type exception: declared as %s but expected %s".format(ctor.args.map(_.name),f_))
        
        checkClassTree( ClassDef(C.superclass) )
        C.checkFields
        C.verifyConstructorArgs
        
        
        OK
      } 					
      
      case Program(cls: List[ClassDef], expr: Expr) => throw TypeError("Found a program declaration inside the program: " + tree)
      case Assign(obj: String, field: String, rhs: Var) => throw TypeError("Unexpected assign declaration: " + tree)
      case FieldDef(tpe: String, name: String) => throw TypeError("Unexpected field declaration: " + tree)
      case CtrDef(name: String, args: List[FieldDef], supers: List[Var], body: List[Assign]) => throw TypeError("Unexpected constructer declaration: " + tree)
      case MethodDef(tpe: String, name: String, args: List[FieldDef], body: Expr) => throw TypeError("Unexpected method declaration: " + tree)

      case _ => throw TypeError("Unable to find type for: %s |- %s".format(ctx,tree))
    }
  }
}

case class EvaluationException(msg: String) extends Exception

object Evaluate extends (Expr => Expr) {

  import Utils._

  def apply(expr: Expr): Expr = apply( expr match {
	    // COMPUTATION
	    // (R-Field)
	    case Select( New(cls: String, args: List[Expr]), field: String) => {
	      val f_ = (Utils getClassDef cls).fieldLookup
	      (f_ zip args).find( _._1.name == field ).get._2
	    }
	    // (R-Invk)
	    case Apply(newI: New, method: String, args: List[Expr]) => {
	      val C = Utils getClassDef newI.cls
	      val m = (C findMethod method).get
	      val e0 = m.body
	      val d_ = args
	      val e_ = m.args
	      substituteInBody(e0, newI, (e_ zip d_) )
	    } 
	    // (R-Cast)
		case Cast(clsD: String, newC:New) if (Utils getClassDef clsD) :> (Utils getClassDef newC.cls) => newC
		
	    // CONGRUENCE
	    // (RC-Field)
	    case Select(obj: Expr, field: String) if apply(obj) != obj => Select(apply(obj), field)
	    // (RC-Invk-Recv)
	    case Apply(obj: Expr, method: String, args: List[Expr]) if apply(obj) != obj => Apply(apply(obj), method, args)
	    // (RC-Invk-Arg)
	    case Apply(obj: Expr, method: String, args: List[Expr]) if args.map(apply(_)) != args => Apply(obj, method, args.map(apply(_)))
	    // (RC-New-Arg)
	    case New(cls: String, args: List[Expr]) if args.map(apply(_)) != args => New(cls, args.map(apply(_)))
	    // (RC-Cast)
	    case Cast(cls: String, e: Expr) => Cast(cls, apply(e))

		case _ => return expr
	  })

  def substituteInBody(exp: Expr, thiss: New, substs: List[(FieldDef, Expr)]): Expr = exp match {
    case Select(obj: Expr, field: String) => Select(substituteInBody(obj, thiss, substs), field)
    case New(cls, args) => New(cls, args map (arg => substituteInBody(arg, thiss, substs)))
    case Cast(cls, e) => Cast(cls, substituteInBody(e, thiss, substs))
    case Var("this") => thiss
    case Var(bd) => substs find (subs => subs._1.name == bd) match {
      case None => exp
      case Some((_, sub)) => sub
    }

    case Apply(obj, method, args) => Apply(substituteInBody(obj, thiss, substs), method, args map (arg => substituteInBody(arg, thiss, substs)))
    case _ => throw new EvaluationException("Apply: Forgot expression " + exp)
  }
}

object CT {

  val objectClass: String = "Object"
  private val objectClassDef = ClassDef(objectClass, null, Nil, CtrDef(objectClass, Nil, Nil, Nil), Nil)

  private var ct: Map[String, ClassDef] = new HashMap[String, ClassDef]

  add(objectClass, objectClassDef)

  def elements = ct iterator

  def lookup(classname: String): Option[ClassDef] = if (classname != null) ct get classname else None

  def add(key: String, element: ClassDef): Unit = ct += key -> element

  def delete(key: String) = ct -= key

  def clear(): Unit = {
    ct clear;
    add(objectClass, objectClassDef)
  }

}

object Utils {
  def getClassDef(className: String): ClassDef = CT lookup className match {
    case None => throw new TypeError("class " + className + " not declared")
    case Some(c: ClassDef) => c
  }
}
